<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

<HTML>

<HEAD>
  <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
  <TITLE>HOL/Algebra/README.html</TITLE>
</HEAD>

<BODY>

<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>

This directory contains proofs in classical algebra.  It is intended
as a base for any algebraic development in Isabelle.  Emphasis is on
reusability.  This is achieved by modelling algebraic structures
as first-class citizens of the logic (not axiomatic type classes, say).
The library is expected to grow in future releases of Isabelle.
Contributions are welcome.

<H2>GroupTheory, including Sylow's Theorem</H2>

<P>These proofs are mainly by Florian Kamm&uuml;ller.  (Later, Larry
Paulson simplified some of the proofs.)  These theories were indeed
the original motivation for locales.

Here is an outline of the directory's contents: <UL> <LI>Theory <A
HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
groups, commutative monoids, commutative groups, homomorphisms and the
subgroup relation.  It also defines the product of two groups
(This theory was reimplemented by Clemens Ballarin).

<LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends
commutative groups by a product operator for finite sets (provided by
Clemens Ballarin).

<LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> defines
the factorization of a group and shows that the factorization a normal
subgroup is a group.

<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
defines bijections over sets and operations on them and shows that they
are a group.  It shows that automorphisms form a group.

<LI>Theory <A HREF="Exponent.html"><CODE>Exponent</CODE></A> the
	    combinatorial argument underlying Sylow's first theorem.

<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
contains a proof of the first Sylow theorem.
</UL>

<H2>Rings and Polynomials</H2>

<UL><LI>Theory <A HREF="Ring.html"><CODE>CRing</CODE></A>
defines Abelian monoids and groups.  The difference to commutative
      structures is merely notational:  the binary operation is
      addition rather than multiplication.  Commutative rings are
      obtained by inheriting properties from Abelian groups and
      commutative monoids.  Further structures in the algebraic
      hierarchy of rings: integral domain.

<LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>
introduces the notion of a R-left-module over an Abelian group, where
	R is a ring.

<LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>
constructs univariate polynomials over rings and integral domains.
	  Degree function.  Universal Property.
</UL>

<H2>Development of Polynomials using Type Classes</H2>

<P>A development of univariate polynomials for HOL's ring classes
is available at <CODE>HOL/Library/Polynomial</CODE>.

<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.

<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
  Author's PhD thesis, 1999.  Also University of Cambridge, Computer Laboratory Technical Report number 473.

<ADDRESS>
<P><A HREF="http://www21.in.tum.de/~ballarin">Clemens Ballarin</A>.
</ADDRESS>
</BODY>
</HTML>
